/**
 * 
 */
package edu.arizona.bio5.onto.decomposition.locality;

import java.util.ArrayList;
import java.util.Collection;
import java.util.Collections;
import java.util.HashSet;
import java.util.List;
import java.util.Set;

import org.semanticweb.owlapi.model.OWLAxiom;
import org.semanticweb.owlapi.model.OWLEntity;

import uk.ac.manchester.cs.owlapi.modularity.ModuleType;
import uk.ac.manchester.cs.util.CrossProductIterator;
import uk.ac.manchester.cs.util.SetUtils;

import com.clarkparsia.owlapi.modularity.locality.LocalityClass;

import edu.arizona.bio5.onto.decomposition.Atom;
import edu.arizona.bio5.onto.decomposition.AtomicDecomposition;
import edu.arizona.bio5.onto.decomposition.MSSLabel;

/**
 * Tries to find as many seed signatures for a principal ideal as possible.
 * 
 * Does NOT guarantee minimality of seed signatures.
 * 
 * This class sets SeedSigBasedLabel labels to the given atom and the lower atoms.
 *
 * (c) Pavel Klinov
 *
 */
public class PISeedSignatureFinder {

	private static final long REFINEMENT_TIMEOUT = 5000;
	
	private ModuleType m_modType = null;
	
	public PISeedSignatureFinder(ModuleType mType) {
		
		m_modType = mType;
	}
	
	public ModuleType getModuleType() {
		
		return m_modType;
	}
	
	protected MSSLabel getMSSLabel(Atom atom) {
		return (MSSLabel) atom.getLabel(MSSLabel.TYPE); 
	}	
	
	/*
	 * Finds all minimal (w.r.t. set inclusion) subsets of the base signature which are seed signatures for the module
	 */
	public Collection<Set<OWLEntity>> findMinSeedSignatures(Atom atom, AtomicDecomposition ad) {
		//See if the label is already assigned
		MSSLabel label = getMSSLabel(atom);
		
		if (label != null) return label.getSeedSignatures();
		
		//First, collect NLS for every axiom in the atom
		Collection<Set<OWLEntity>> seedSigs = getAtomNonLocalitySignatures(atom);
		boolean complete = true;
		
		if (!ad.isBottomAtom(atom)) {
			//Recursive step
			//Need to combine the NLS for the current atom with MSS for the atoms it depends on
			//First, find those MSS recursively
			for (Atom lowerAtom : ad.getDependencies(atom, true)) {
				
				if (getMSSLabel(lowerAtom) == null) {
					//Label will be assigned to the lower atom
					findMinSeedSignatures(lowerAtom, ad);
				}
				
				complete &= getMSSLabel(lowerAtom).isComplete();
			}
			//Now, do the combination
			//System.out.print("Combination starts...");
			
			complete &= combineNLSwithMSSes(atom, ad, seedSigs);
			
			//System.out.println("...ends");
		}
		
		atom.setLabel(new MSSLabel(seedSigs, complete));
		
		return seedSigs;
	}	
	
	/*
	 * The key method
	 * Combines the set of all min signatures that make at least on axiom in the current atom non-local
	 * with
	 * sets of minimal seed signatures for its lower atoms
	 */
	private boolean combineNLSwithMSSes(Atom atom, AtomicDecomposition ad, Collection<Set<OWLEntity>> nlSigs) {
		
		Collection<Set<OWLEntity>> mss = new ArrayList<Set<OWLEntity>>(nlSigs.size());
		boolean complete = true;
		
		for (Set<OWLEntity> nlSig : nlSigs) {
			
			complete &= transformNonLocalitySignature(nlSig, atom, ad, mss);
		}
		
		nlSigs.clear();
		nlSigs.addAll(mss);
		
		return complete;
	}

	/*
	 * Analyzes how a current non-locality signature for the top atom
	 * can be complemented by a set of seed signatures which  pull one or more lower atoms
	 * such that the enlarged signature covers the original NL signature
	 */
	private boolean transformNonLocalitySignature(Set<OWLEntity> nlSig, Atom atom, AtomicDecomposition ad, Collection<Set<OWLEntity>> mss) {
		
		boolean complete = true;
		//First, see which lower ideals have terms from the NL signature
		List<Atom> relLowerAtoms = new ArrayList<Atom>();

		for (Atom lowerAtom : ad.getDependencies(atom, true)) {
			//FIXME Obviously slow, this needs to be cached
			if (!SetUtils.intersection(nlSig, ad.getPrincipalIdealSignature(lowerAtom)).isEmpty()) {
				
				relLowerAtoms.add(lowerAtom);
			}
		}
		//No lower atom uses any terms from the current NL signature of the top atom
		//so it can't be refined
		mss.add(nlSig);
		//Now we go through the powerset of relLowerAtoms
		//We go bottom-up, should be able to do some dynamic programming later
		//Give up completeness if the process is taking too long;
		for (int k = 1; k <= relLowerAtoms.size(); k++) {
			
			long startTime = System.currentTimeMillis();
			
			for (Set<Atom> lowerSubset : SetUtils.kSubsets(relLowerAtoms, k)) {
				//Split the NL signature onto two parts:
				//Terms that come from the atoms in lowerSubset
				//Terms that come from the top atom (call it nlSigFromTop)
				Set<OWLEntity> lowerAtomsSig = getUnionPISignature(lowerSubset, ad);
				Set<OWLEntity> nlSigFromTop = SetUtils.difference(nlSig, lowerAtomsSig);
				//An MSS candidate signature is nlSigFromTop union X
				//where X contains one min seed signature for every atom in lowerSubsets
				for (CrossProductIterator<Set<OWLEntity>> iter = getIteratorOverMSSCrossProduct(lowerSubset); iter.hasNext();) {
					
					Set<OWLEntity> crossProductElem = SetUtils.union(iter.next());
					//!!WARNING!! crossProductElem may be a non-minimal seed signature for atoms in lowerSubset
					//because of horizontal (weak) dependencies between them
					//So we need to minimize it
					Set<OWLEntity> mssCandidate = SetUtils.union(nlSigFromTop, crossProductElem);
					
					SetUtils.addAndMinimizeWrtInclusion(mssCandidate, mss);
					
					if ((System.currentTimeMillis() - startTime) > REFINEMENT_TIMEOUT) {
						
						complete = false;
						break;
					}
				}
				
				if ((System.currentTimeMillis() - startTime) > REFINEMENT_TIMEOUT) {
					
					complete = false;
					break;
				}				
			}
		}
		
		return complete/* && (relLowerAtoms.size() <= MAX_LOWER_ATOM_NUM)*/;
	}

	/*
	 * Unions signatures of principal ideals
	 */
	private Set<OWLEntity> getUnionPISignature(Set<Atom> atoms, AtomicDecomposition ad) {

		Set<OWLEntity> unionSig = new HashSet<OWLEntity>();
		
		for (Atom atom : atoms) unionSig.addAll(ad.getPrincipalIdealSignature(atom));
		
		return unionSig;
	}

	private CrossProductIterator<Set<OWLEntity>> getIteratorOverMSSCrossProduct(Set<Atom> atoms) {
		
		Collection<Collection<Set<OWLEntity>>> mssList = new ArrayList<Collection<Set<OWLEntity>>>(atoms.size());
		
		for (Atom atom : atoms) mssList.add(getMSSLabel(atom).getSeedSignatures());

		return new CrossProductIterator<Set<OWLEntity>>(mssList);
	}

	/*
	 * Finds all signatures which make at least one axiom in the atom non-local
	 */
	protected Collection<Set<OWLEntity>> getAtomNonLocalitySignatures(Atom atom) {
		
		Collection<Set<OWLEntity>> minSeedSigs = new ArrayList<Set<OWLEntity>>();
		//Find all signatures s.t. at least one axiom is non-local
		for (OWLAxiom axiom : atom.getAxioms()) {
			
			SetUtils.addAllandMinimizeWrtInclusion(findNonLocalitySigs(axiom, atom.getSignature()), minSeedSigs);
			//minSeedSigs.addAll(findNonLocalitySigs(axiom, atom.getSignature()));
			
			if (minSeedSigs.contains(Collections.emptySet())) break;
		}
		
		return minSeedSigs;
	}
	
	protected Collection<Set<OWLEntity>> findNonLocalitySigs(OWLAxiom axiom, Set<OWLEntity> baseSig) {
		
		NonSyntLocalAxiomSignatureFinder topNLSFinder = new NonSyntLocalAxiomSignatureFinder(LocalityClass.TOP_TOP);
		NonSyntLocalAxiomSignatureFinder botNLSFinder = new NonSyntLocalAxiomSignatureFinder(LocalityClass.BOTTOM_BOTTOM);
		
		Collection<Set<OWLEntity>> nls = null;
		
		switch (m_modType) {
		
		case BOT: 
			nls = botNLSFinder.findMinimalSeedSignatures(axiom, baseSig);
			break;
		case TOP: 
			nls = topNLSFinder.findMinimalSeedSignatures(axiom, baseSig);
			break;
		case STAR:
			nls = botNLSFinder.findMinimalSeedSignatures(axiom, baseSig);
			nls = SetUtils.unionAllAndMinimizeWrtInclusion(topNLSFinder.findMinimalSeedSignatures(axiom, baseSig), nls);
			break;
		default:
			throw new RuntimeException("Unsupported notion of syntactic modularity:" + m_modType);
		}

		return nls;
	}	
}
